(*
** Prueba de correccion de Mini-AES.
** Esto es, encriptar y desencriptar retorna el mismo texto.
** Incluye tambien los lemas auxiliares para cada operacion de Mini-AES.
*)

Require Import Lang.
Require Import TypesImpl.
Require Import Matrix.
Require Import MiniAes.
Import LangImpl.
Load Util.

(******************
   PARAMETROS
******************)
Definition mid := id 101.
Definition mult_table_id := id 102.
Definition kid0 := id 103.
Definition kid1 := id 104.
Definition kid2 := id 105.
Definition mini_sbox_id := id 106.
Definition mini_sbox_inv_id := id 107.

Variable mini_sbox mini_sbox_inv: Matrix Byte 1 16.
Parameter mult_table: Matrix Byte 16 16.
Parameters key0 key1 key2: Matrix Byte 2 2.
Parameters k0_00 k0_01 k0_10 k0_11 k1_00 k1_01 k1_10 k1_11 k2_00 k2_01 k2_10 k2_11 s00 s01 s10 s11:Byte.

Parameter k0_defined : 0 <= k0_00 < 16 /\
                       0 <= k0_01 < 16 /\
                       0 <= k0_10 < 16 /\
                       0 <= k0_11 < 16.

Parameter k1_defined : 0 <= k1_00 < 16 /\
                       0 <= k1_01 < 16 /\
                       0 <= k1_10 < 16 /\
                       0 <= k1_11 < 16.

Parameter k2_defined : 0 <= k2_00 < 16 /\
                       0 <= k2_01 < 16 /\
                       0 <= k2_10 < 16 /\
                       0 <= k2_11 < 16.

Notation "'get'" := matrix_get.
Notation "'set'" := matrix_set.
Notation "'xor'" := byte_xor.

Open Scope Z_scope.

Ltac destruct_and :=
  match goal with
    | [ H1 : _ /\ _ |- _ ] => destruct H1
  end
.

Ltac destruct_cases :=
  match goal with
    | [H1 : Gt = Lt |- _] => discriminate H1

    | [H1 : Eq = Lt |- _] => discriminate H1

    | [H1 : 0 <= Z.neg _ |- _] => compute in H1; destruct H1; reflexivity

    | [H1 : match ?p with
       | (_~1)%positive => Gt
       | (_~0)%positive => Gt
       | 1%positive => Gt
       end = Lt |- _] => destruct p; discriminate H1; elim H1

    | [H1: match ?p with
             | (_~1)%positive => Gt
             | (_~0)%positive => Gt
             | 1%positive => Eq
           end = Lt |- _] => destruct p; discriminate H1; elim H1

    | [H1 : Z.pos _ < 16, p: positive  |- _] => destruct p; compute in H1

    | [H1 : _ = Lt, p: positive  |- _] => destruct p; compute in H1

    | [H1 : get Byte ?m ?n ?i ?j ?matr = Some _, H2: get Byte ?m ?n ?i ?j ?matr = _ |- _] =>
      rewrite H1 in H2; injection H2; intros; subst; assumption
  end
.

Theorem mini_sbox_inverse : forall x y,
  sbox_defined mini_sbox -> sbox_inv_defined mini_sbox_inv -> 0 <= x < 16 -> get Byte 1 16 0 x mini_sbox = Some y -> get Byte 1 16 0 y mini_sbox_inv = Some x.
Proof.
  intros x y Hsbox HinvSbox Hx H.
  unfold sbox_defined in Hsbox.
  unfold sbox_inv_defined in HinvSbox.
  repeat destruct_and.
  destruct x; repeat destruct_cases.
Qed.

Ltac mult_table_cases :=
  match goal with
    | [H1 : Gt = Lt |- _] => discriminate H1

    | [H1 : Eq = Lt |- _] => discriminate H1

    | [H1 : 0 <= Z.neg _ |- _] => compute in H1; destruct H1; reflexivity

    | [H1 : match ?p with
       | (_~1)%positive => Gt
       | (_~0)%positive => Gt
       | 1%positive => Gt
       end = Lt |- _] => destruct p; discriminate H1; elim H1

    | [H1: match ?p with
             | (_~1)%positive => Gt
             | (_~0)%positive => Gt
             | 1%positive => Eq
           end = Lt |- _] => destruct p; discriminate H1; elim H1

    | [H1 : Z.pos _ < 16, p: positive  |- _] => destruct p; compute in H1

    | [H1 : _ = Lt, p: positive  |- _] => destruct p; compute in H1

    | [H1 : get Byte ?m ?n ?i ?j ?matr = Some _, H2: get Byte ?m ?n ?i ?j ?matr = _ |- _] =>
      rewrite H1 in H2; injection H2; intros; subst

    | _ => split; assumption
  end
.

Theorem mult_table_inv : forall x1 x2 x3 x4,
  mult_table_defined mult_table -> 0 <= x1 < 16 -> 0 <= x2 < 16 -> get Byte 16 16 x1 x2 mult_table = Some x3 -> matrix_get Byte 16 16 x2 x1 mult_table = Some x4 ->
      (get Byte 16 16 x3 x4 mult_table = Some x1 /\ get Byte 16 16 x4 x3 mult_table = Some x2).
Proof.
(* La prueba esta hecha pero consume mucha memoria por los 256 casos *)
(*  intros.
  unfold mult_table_defined in H.
  repeat destruct_and.
  destruct x1,x2; repeat multable_cases.
Qed.*)
Admitted.

Ltac aux_tac :=
  match goal with
    | [H1 : Gt = Lt |- _] => discriminate H1

    | [H1 : Eq = Lt |- _] => discriminate H1

    | [H1 : 0 <= Z.neg _ |- _] => compute in H1; destruct H1; reflexivity

    | [H1 : match ?p with
       | (_~1)%positive => Gt
       | (_~0)%positive => Gt
       | 1%positive => Gt
       end = Lt |- _] => destruct p; discriminate H1; elim H1

    | [H1: match ?p with
             | (_~1)%positive => Gt
             | (_~0)%positive => Gt
             | 1%positive => Eq
           end = Lt |- _] => destruct p; discriminate H1; elim H1

    | [H1 : Z.pos _ < 16, p: positive  |- _] => destruct p; compute in H1

    | [H1 : _ = Lt, p: positive  |- _] => destruct p; compute in H1

    | [H1 : get Byte ?m ?n ?i ?j ?matr = Some _, H2: get Byte ?m ?n ?i ?j ?matr = _ |- _] =>
      rewrite H1 in H2; injection H2; intros; subst; omega
  end
.

Theorem mini_sbox_result : forall x y, sbox_defined mini_sbox -> 0 <= x < 16 -> get Byte 1 16 0 x mini_sbox = Some y -> 0 <= y < 16.
Proof.
intros.
unfold sbox_defined in H.
repeat destruct_and.
destruct x; repeat aux_tac.
Qed.

Theorem mini_sbox_inv_result : forall x y, sbox_inv_defined mini_sbox_inv -> 0 <= x < 16 -> get Byte 1 16 0 x mini_sbox_inv = Some y -> 0 <= y < 16.
Proof.
intros.
unfold sbox_inv_defined in H.
repeat destruct_and.
destruct x; repeat aux_tac.
Qed.

Theorem mult_table_result : forall x y z, mult_table_defined mult_table -> 0 <= x < 16 -> 0 <= y < 16 -> get Byte 16 16 x y mult_table = Some z -> 0 <= z < 16.
(* La prueba esta hecha pero consume mucha memoria por los 256 casos *)
(* 
Proof.
intros.
unfold mult_table_defined in H.
repeat destruct_and.
destruct x,y; repeat aux_tac.
Qed.*)
Admitted.

Definition invariants (st:State):=
    st mini_sbox_id = Some (byte_matrix_val mini_sbox) /\
    st mini_sbox_inv_id = Some (byte_matrix_val mini_sbox_inv) /\
    st mult_table_id = Some (byte_matrix_val mult_table) /\
    st kid0 = Some (byte_matrix_val key0) /\
    st kid1 = Some (byte_matrix_val key1) /\
    st kid2 = Some (byte_matrix_val key2) /\
    matrix_defined key0 k0_00 k0_01 k0_10 k0_11  /\
    matrix_defined key1 k1_00 k1_01 k1_10 k1_11  /\
    matrix_defined key2 k2_00 k2_01 k2_10 k2_11  /\
    sbox_defined mini_sbox /\
    sbox_inv_defined mini_sbox_inv
.

Theorem hoare_matrix_xor_00 : forall (mid kid:Id)(key: Matrix Byte 2 2)(m00 m01 m10 m11 k00 k01 k10 k11: Byte),
                              equal_id mid kid = false -> equal_id mid mini_sbox_id = false ->  
                              equal_id mid mini_sbox_inv_id = false -> equal_id mid mult_table_id = false ->
                              equal_id mid kid0 = false ->  
                              equal_id mid kid1 = false -> equal_id mid kid2 = false ->
    {{ fun st => exists (matr: Matrix Byte 2 2), 
                 st mid = Some (byte_matrix_val matr) /\
                 matrix_defined matr m00 m01 m10 m11 /\
                 st kid = Some (byte_matrix_val key) /\
                 matrix_defined key k00 k01 k10 k11 /\
                 invariants st }}
      instr_matrix_set mid 0 0 (byte_exp_xor (byte_exp_matrix mid 0 0) (byte_exp_matrix kid 0 0))
    {{ fun st => exists (matr': Matrix Byte 2 2),
                 st mid = Some (byte_matrix_val matr') /\
                 matrix_defined matr' (xor m00 k00) m01 m10 m11 /\
                 st kid = Some (byte_matrix_val key) /\
                 matrix_defined key k00 k01 k10 k11 /\
                 invariants st }}.
Proof.
intros until 0. intros T0 T1 T2 T3 T4 T5 T6.
eapply hoare_consequence_pre.
apply hoare_matrix_set.
intros st H0 m n matr1 matr2 i j b H1 H2 H3 H4 H5.
elim H0. intros. clear H0.
elim (set_matrix 0 0 2 2 x b). intros.
exists x0.
inversion H1; subst. clear H1.
inversion H2; subst. clear H2.
inversion_clear H4.
destruct H.
rewrite H1 in H.
injection H; intros; subst. clear H4.
assert (x = matr1).
apply matrix_some_eq.
symmetry. exact H.
subst.
inversion H3. subst. clear H3.
inversion H8. subst. clear H8.
inversion H9. subst. clear H9.
inversion H14. subst. clear H14.
inversion H15. subst. clear H15.
inversion H11. subst. clear H11.
inversion H12. subst. clear H12.
inversion_clear H10.
rewrite H3 in H1.
injection H1; intros; subst. clear H4.
assert (matr = matr1).
apply matrix_some_eq. auto.
rewrite H4 in H7.
destruct H2.
destruct H6.

unfold matrix_defined in H2.
destruct H2.

assert (Some b1 = Some m00).
rewrite <- H2. rewrite <- H7.
reflexivity.
injection H11; intros; subst.
inversion_clear H13.
rewrite H4 in H6.

injection H6; intros; subst. clear H12.
assert (matr0 = key).
apply matrix_some_eq. auto. subst.

assert (Some b2 = Some k00).
destruct H9.
destruct H9.
rewrite <- H9. rewrite <- H8.
reflexivity.
injection H12; intros; subst.

assert (Some matr2 = Some x0).
rewrite <- H0. rewrite <- H5.
reflexivity.
injection H13; intros. subst.
clear H1 H6 H11 H12 H13.
unfold update.
split.
destruct (equal_id mid0 mid0) eqn:?. clear Heqb.
reflexivity.
destruct mid0.
unfold equal_id in *.
elim (beq_nat_false n n); auto.
split.

apply (matrix_get_set_00 matr1 x0 m00 m01 m10 m11 (xor m00 k00)).
unfold matrix_defined.
split.
assumption. assumption.
assumption.


split.
rewrite T0.
assumption.

unfold invariants; split.
apply H9.

split.
rewrite T1.
apply H9.

split.
rewrite T2.
apply H9.

split.
rewrite T3.
apply H9.

split.
rewrite T4.
apply H9.

split.
rewrite T5.
apply H9.

split.
rewrite T6.
apply H9.

unfold invariants in H9.
apply H9.

omega. omega.
Qed.

Theorem hoare_matrix_xor_01 : forall (mid kid:Id)(key: Matrix Byte 2 2)(m00 m01 m10 m11 k00 k01 k10 k11: Byte),
                              equal_id mid kid = false -> equal_id mid mini_sbox_id = false ->  
                              equal_id mid mini_sbox_inv_id = false -> equal_id mid mult_table_id = false ->
                              equal_id mid kid0 = false ->  
                              equal_id mid kid1 = false -> equal_id mid kid2 = false ->
    {{ fun st => exists (matr: Matrix Byte 2 2), 
                 st mid = Some (byte_matrix_val matr) /\
                 matrix_defined matr m00 m01 m10 m11 /\
                 st kid = Some (byte_matrix_val key) /\
                 matrix_defined key k00 k01 k10 k11 /\
                 invariants st }}
      instr_matrix_set mid 0 1 (byte_exp_xor (byte_exp_matrix mid 0 1) (byte_exp_matrix kid 0 1))
    {{ fun st => exists (matr': Matrix Byte 2 2),
                 st mid = Some (byte_matrix_val matr') /\
                 matrix_defined matr'  m00 (xor m01 k01) m10 m11 /\
                 st kid = Some (byte_matrix_val key) /\
                 matrix_defined key k00 k01 k10 k11 /\
                 invariants st }}.
Proof.
intros until 0. intros T0 T1 T2 T3 T4 T5 T6.
eapply hoare_consequence_pre.
apply hoare_matrix_set.
intros st H0 m n matr1 matr2 i j b H1 H2 H3 H4 H5.
elim H0. intros. clear H0.
elim (set_matrix 0 1 2 2 x b). intros.
exists x0.
inversion H1; subst. clear H1.
inversion H2; subst. clear H2.
inversion_clear H4.
destruct H.
rewrite H1 in H.
injection H; intros; subst. clear H4.
assert (x = matr1).
apply matrix_some_eq.
symmetry. exact H.
subst.
inversion H3. subst. clear H3.
inversion H8. subst. clear H8.
inversion H9. subst. clear H9.
inversion H14. subst. clear H14.
inversion H15. subst. clear H15.
inversion H11. subst. clear H11.
inversion H12. subst. clear H12.
inversion_clear H10.
rewrite H3 in H1.
injection H1; intros; subst. clear H4.
assert (matr = matr1).
apply matrix_some_eq. auto.
rewrite H4 in H7.
destruct H2.
destruct H6.

unfold matrix_defined in H2.
destruct H2.

assert (Some b1 = Some m01).
destruct H10.
rewrite <- H10. rewrite <- H7.
reflexivity.
injection H11; intros; subst.
inversion_clear H13.
rewrite H4 in H6.

injection H6; intros; subst. clear H12.
assert (matr0 = key).
apply matrix_some_eq. auto. subst.

assert (Some b2 = Some k01).
destruct H9.
destruct H9.
destruct H13.
rewrite <- H13. rewrite <- H8.
reflexivity.
injection H12; intros; subst.

assert (Some matr2 = Some x0).
rewrite <- H0. rewrite <- H5.
reflexivity.
injection H13; intros. subst.
clear H1 H6 H11 H12 H13.
unfold update.
split.
destruct (equal_id mid0 mid0) eqn:?. clear Heqb.
reflexivity.
destruct mid0.
unfold equal_id in *.
elim (beq_nat_false n n); auto.
split.

apply (matrix_get_set_01 matr1 x0 m00 m01 m10 m11 (xor m01 k01)).
unfold matrix_defined.
split.
assumption. assumption.
assumption.


split.
rewrite T0.
assumption.

unfold invariants; split.
apply H9.

split.
rewrite T1.
apply H9.

split.
rewrite T2.
apply H9.

split.
rewrite T3.
apply H9.

split.
rewrite T4.
apply H9.

split.
rewrite T5.
apply H9.

split.
rewrite T6.
apply H9.

unfold invariants in H9.
apply H9.

omega. omega.
Qed.

Theorem hoare_matrix_xor_10 : forall (mid kid:Id)(key: Matrix Byte 2 2)(m00 m01 m10 m11 k00 k01 k10 k11: Byte),
                              equal_id mid kid = false -> equal_id mid mini_sbox_id = false ->  
                              equal_id mid mini_sbox_inv_id = false -> equal_id mid mult_table_id = false ->
                              equal_id mid kid0 = false ->  
                              equal_id mid kid1 = false -> equal_id mid kid2 = false ->
    {{ fun st => exists (matr: Matrix Byte 2 2), 
                 st mid = Some (byte_matrix_val matr) /\
                 matrix_defined matr m00 m01 m10 m11 /\
                 st kid = Some (byte_matrix_val key) /\
                 matrix_defined key k00 k01 k10 k11 /\
                 invariants st }}
      instr_matrix_set mid 1 0 (byte_exp_xor (byte_exp_matrix mid 1 0) (byte_exp_matrix kid 1 0))
    {{ fun st => exists (matr': Matrix Byte 2 2),
                 st mid = Some (byte_matrix_val matr') /\
                 matrix_defined matr'  m00 m01 (xor m10 k10) m11 /\
                 st kid = Some (byte_matrix_val key) /\
                 matrix_defined key k00 k01 k10 k11 /\
                 invariants st }}.
Proof.
intros until 0. intros T0 T1 T2 T3 T4 T5 T6.
eapply hoare_consequence_pre.
apply hoare_matrix_set.
intros st H0 m n matr1 matr2 i j b H1 H2 H3 H4 H5.
elim H0. intros. clear H0.
elim (set_matrix 1 0 2 2 x b). intros.
exists x0.
inversion H1; subst. clear H1.
inversion H2; subst. clear H2.
inversion_clear H4.
destruct H.
rewrite H1 in H.
injection H; intros; subst. clear H4.
assert (x = matr1).
apply matrix_some_eq.
symmetry. exact H.
subst.
inversion H3. subst. clear H3.
inversion H8. subst. clear H8.
inversion H9. subst. clear H9.
inversion H14. subst. clear H14.
inversion H15. subst. clear H15.
inversion H11. subst. clear H11.
inversion H12. subst. clear H12.
inversion_clear H10.
rewrite H3 in H1.
injection H1; intros; subst. clear H4.
assert (matr = matr1).
apply matrix_some_eq. auto.
rewrite H4 in H7.
destruct H2.
destruct H6.

unfold matrix_defined in H2.
destruct H2.

assert (Some b1 = Some m10).
destruct H10.
destruct H11.

rewrite <- H11. rewrite <- H7.
reflexivity.
injection H11; intros; subst.
inversion_clear H13.
rewrite H4 in H6.

injection H6; intros; subst. clear H12.
assert (matr0 = key).
apply matrix_some_eq. auto. subst.

assert (Some b2 = Some k10).
destruct H9.
destruct H9.
destruct H13.
destruct H14.
rewrite <- H14. rewrite <- H8.
reflexivity.
injection H12; intros; subst.

assert (Some matr2 = Some x0).
rewrite <- H0. rewrite <- H5.
reflexivity.
injection H13; intros. subst.
clear H1 H6 H11 H12 H13.
unfold update.
split.
destruct (equal_id mid0 mid0) eqn:?. clear Heqb.
reflexivity.
destruct mid0.
unfold equal_id in *.
elim (beq_nat_false n n); auto.
split.

apply (matrix_get_set_10 matr1 x0 m00 m01 m10 m11 (xor m10 k10)).
unfold matrix_defined.
split.
assumption. assumption.
assumption.


split.
rewrite T0.
assumption.

unfold invariants; split.
apply H9.

split.
rewrite T1.
apply H9.

split.
rewrite T2.
apply H9.

split.
rewrite T3.
apply H9.

split.
rewrite T4.
apply H9.

split.
rewrite T5.
apply H9.

split.
rewrite T6.
apply H9.

unfold invariants in H9.
apply H9.

omega. omega.
Qed.

Theorem hoare_matrix_xor_11 : forall (mid kid:Id)(key: Matrix Byte 2 2)(m00 m01 m10 m11 k00 k01 k10 k11: Byte),
                    equal_id mid kid = false ->
                    equal_id mid mini_sbox_id = false ->  
                    equal_id mid mini_sbox_inv_id = false ->
                    equal_id mid mult_table_id = false ->
                    equal_id mid kid0 = false ->  
                    equal_id mid kid1 = false ->
                    equal_id mid kid2 = false ->
    {{ fun st => exists (matr: Matrix Byte 2 2), 
                 st mid = Some (byte_matrix_val matr) /\
                 matrix_defined matr m00 m01 m10 m11 /\
                 st kid = Some (byte_matrix_val key) /\
                 matrix_defined key k00 k01 k10 k11 /\
                 invariants st }}
      instr_matrix_set mid 1 1 (byte_exp_xor (byte_exp_matrix mid 1 1) (byte_exp_matrix kid 1 1))
    {{ fun st => exists (matr': Matrix Byte 2 2),
                 st mid = Some (byte_matrix_val matr') /\
                 matrix_defined matr'  m00 m01 m10 (xor m11 k11) /\
                 st kid = Some (byte_matrix_val key) /\
                 matrix_defined key k00 k01 k10 k11 /\
                 invariants st }}.
Proof.
intros until 0. intros T0 T1 T2 T3 T4 T5 T6.
eapply hoare_consequence_pre.
apply hoare_matrix_set.

intros st H0 m n matr1 matr2 i j b H1 H2 H3 H4 H5.
elim H0; intros; clear H0.
elim (set_matrix 1 1 2 2 x b); [intros | omega | omega].

inversion H1; subst. clear H1.
inversion H2; subst. clear H2.
inversion_clear H4.
destruct H.
rewrite H1 in H.
injection H; intros; subst. clear H4.
assert (x = matr1).
apply matrix_some_eq.
symmetry. exact H.
subst.
inversion H3; subst. clear H3.
inversion H8; subst. clear H8.
inversion H9; subst. clear H9.
inversion H14; subst. clear H14.
inversion H15; subst. clear H15.
inversion H11; subst. clear H11.
inversion H12; subst. clear H12.
inversion_clear H10.
rewrite H3 in H1.
injection H1; intros; subst. clear H4.
assert (matr = matr1).
apply matrix_some_eq. auto.
rewrite H4 in H7.
destruct H2.
destruct H6.
unfold matrix_defined in H2.
destruct H2.
assert (Some b1 = Some m11).
destruct H10.
destruct H11.
rewrite <- H12. rewrite <- H7.
reflexivity.
injection H11; intros; subst.
inversion_clear H13.
rewrite H4 in H6.
injection H6; intros; subst. clear H12.
assert (matr0 = key).
apply matrix_some_eq. auto. subst.
assert (Some b2 = Some k11).
destruct H9.
destruct H9.
destruct H13.
destruct H14.
rewrite <- H15. rewrite <- H8.
reflexivity.
injection H12; intros; subst.
clear H1 H6 H11 H12.
exists matr2.
unfold update.

split.
destruct (equal_id mid0 mid0) eqn:?. clear Heqb.
reflexivity.
destruct mid0.
unfold equal_id in Heqb.
elim (beq_nat_false n n); auto.

split.
apply (matrix_get_set_11 matr1 matr2 m00 m01 m10 m11 (xor m11 k11)).
split; assumption.
exact H5.

split.
rewrite T0.
assumption.

unfold invariants; split.
apply H9.

split.
rewrite T1.
apply H9.

split.
rewrite T2.
apply H9.

split.
rewrite T3.
apply H9.

split.
rewrite T4.
apply H9.

split.
rewrite T5.
apply H9.

split.
rewrite T6.
apply H9.

unfold invariants in H9.
apply H9.
Qed.

Ltac equal_id_false :=
  match goal with
    | |- equal_id ?x ?y = false => unfold x; unfold y; compute; reflexivity
  end
. 

Lemma hoare_key_addition : forall m00 m01 m10 m11 kid k00 k01 k10 k11 key,
               equal_id mid kid = false ->
     {{ fun st => exists (matr: Matrix Byte 2 2),
                  matrix_defined key k00 k01 k10 k11 /\
                  st mid = Some (byte_matrix_val matr) /\
                  matrix_defined matr m00 m01 m10 m11 /\
                  st kid = Some (byte_matrix_val key) /\
                  invariants st }}
     MiniAes.key_addition mid kid
     {{ fun st => exists (newMatr: Matrix Byte 2 2),
                  st mid = Some (byte_matrix_val newMatr) /\
                  matrix_defined newMatr (xor m00 k00) (xor m01 k01) (xor m10 k10) (xor m11 k11) /\
                  invariants st }}.
Proof.
intros until 0; intro T.
unfold MiniAes.key_addition.

eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_matrix_xor_00; try equal_id_false.
assumption.

intros st H.
elim H; intros.
exists x.
split. apply H0.
split. apply H0.
split. apply H0.
split. apply H0.
apply H0.

eapply hoare_seq.
apply hoare_matrix_xor_01; try equal_id_false.
assumption.

eapply hoare_seq.
apply hoare_matrix_xor_10; try equal_id_false.
assumption.

eapply hoare_consequence_post.
apply hoare_matrix_xor_11; try equal_id_false.
assumption.

intros st H1.
elim H1; intros.
exists x.
split. apply H.
split. apply H.
apply H.
Qed.

Theorem hoare_byte_matrix_asgn_00 : forall (mid X: Id) m00 m01 m10 m11, 
                                    equal_id X mid = false -> 
                                    equal_id X mini_sbox_id = false -> 
                                    equal_id X mini_sbox_inv_id = false ->
                                    equal_id X mult_table_id = false ->
                                    equal_id X kid0 = false ->  
                                    equal_id X kid1 = false -> 
                                    equal_id X kid2 = false ->
  {{ fun st => exists (matr: Matrix Byte 2 2),
               st mid = Some (byte_matrix_val matr) /\
               matrix_defined matr m00 m01 m10 m11 /\
               invariants st }}
      byte X ::= (byte_exp_matrix mid 0 0)
  {{ fun st => exists (matr: Matrix Byte 2 2),
               st X = Some (byte_val m00) /\
               st mid = Some (byte_matrix_val matr) /\
               matrix_defined matr m00 m01 m10 m11 /\
               invariants st}}.
Proof.
intros until 0. intros H T1 T2 T3 T4 T5 T6.
eapply hoare_consequence_pre.
apply hoare_asgn.
intros st H1 bb H2.
elim H1; intros x H0; clear H1.
exists x.
split; unfold update.
destruct (equal_id X X) eqn:?. clear Heqb.
inversion H2; subst. clear H2.
inversion H6; subst. clear H6.
inversion H7; subst. clear H7.
inversion H8; subst. clear H8.
destruct H0.
rewrite H2 in H0.
injection H0. intros. subst. clear H3.
assert (matr = x).
apply matrix_some_eq.
assumption.
rewrite H3 in H5.
destruct H1.
destruct H1.
assert (Some bb = Some m00).
rewrite <- H1.
rewrite <- H5.
reflexivity.
injection H7; intros.
rewrite H8; reflexivity.

destruct X.
unfold equal_id in *.
elim (beq_nat_false n n); auto.

split.
destruct (equal_id X mid0) eqn:?.
inversion H.
apply H0.

split.
apply H0.

unfold invariants; split.

rewrite T1.
apply H0.

split.
rewrite T2.
apply H0.

split.
rewrite T3.
apply H0.

split.
rewrite T4.
apply H0.

split.
rewrite T5.
apply H0.

split.
rewrite T6.
apply H0.

unfold invariants in H0.
apply H0.
Qed.

Theorem hoare_byte_matrix_asgn_01 : forall (mid X: Id) m00 m01 m10 m11, 
                                    equal_id X mid = false -> 
                                    equal_id X mini_sbox_id = false -> 
                                    equal_id X mini_sbox_inv_id = false ->
                                    equal_id X mult_table_id = false ->
                                    equal_id X kid0 = false ->  
                                    equal_id X kid1 = false -> 
                                    equal_id X kid2 = false ->
  {{ fun st => exists (matr: Matrix Byte 2 2),
               st mid = Some (byte_matrix_val matr) /\
               matrix_defined matr m00 m01 m10 m11 /\
               invariants st }}
      byte X ::= (byte_exp_matrix mid 0 1)
  {{ fun st => exists (matr: Matrix Byte 2 2),
               st X = Some (byte_val m01) /\
               st mid = Some (byte_matrix_val matr) /\
               matrix_defined matr m00 m01 m10 m11 /\
               invariants st}}.
Proof.
intros until 0. intros H T1 T2 T3 T4 T5 T6.
eapply hoare_consequence_pre.
apply hoare_asgn.
intros st H1 bb H2.
elim H1; intros x H0; clear H1.
exists x.
split; unfold update.
destruct (equal_id X X) eqn:?. clear Heqb.
inversion H2; subst. clear H2.
inversion H6; subst. clear H6.
inversion H7; subst. clear H7.
inversion H8; subst. clear H8.
destruct H0.
rewrite H2 in H0.
injection H0. intros. subst. clear H3.
assert (matr = x).
apply matrix_some_eq.
assumption.
rewrite H3 in H5.
destruct H1.
destruct H1.
assert (Some bb = Some m01).
destruct H6.
rewrite <- H6.
rewrite <- H5.
reflexivity.
injection H7; intros.
rewrite H8; reflexivity.

destruct X.
unfold equal_id in *.
elim (beq_nat_false n n); auto.

split.
destruct (equal_id X mid0) eqn:?.
inversion H.
apply H0.

split.
apply H0.

unfold invariants; split.

rewrite T1.
apply H0.

split.
rewrite T2.
apply H0.

split.
rewrite T3.
apply H0.

split.
rewrite T4.
apply H0.

split.
rewrite T5.
apply H0.

split.
rewrite T6.
apply H0.

unfold invariants in H0.
apply H0.
Qed.

Lemma hoare_byte_matrix_asgn_10 : forall (mid X: Id) m00 m01 m10 m11, 
                                    equal_id X mid = false -> 
                                    equal_id X mini_sbox_id = false -> 
                                    equal_id X mini_sbox_inv_id = false ->
                                    equal_id X mult_table_id = false ->
                                    equal_id X kid0 = false ->  
                                    equal_id X kid1 = false -> 
                                    equal_id X kid2 = false ->
  {{ fun st => exists (matr: Matrix Byte 2 2),
               st mid = Some (byte_matrix_val matr) /\
               matrix_defined matr m00 m01 m10 m11 /\
               invariants st }}
      byte X ::= (byte_exp_matrix mid 1 0)
  {{ fun st => exists (matr: Matrix Byte 2 2),
               st X = Some (byte_val m10) /\
               st mid = Some (byte_matrix_val matr) /\
               matrix_defined matr m00 m01 m10 m11 /\
               invariants st}}.
Proof.
intros until 0. intros H T1 T2 T3 T4 T5 T6.
eapply hoare_consequence_pre.
apply hoare_asgn.
intros st H1 bb H2.
elim H1; intros x H0; clear H1.
exists x.
split; unfold update.
destruct (equal_id X X) eqn:?. clear Heqb.
inversion H2; subst. clear H2.
inversion H6; subst. clear H6.
inversion H7; subst. clear H7.
inversion H8; subst. clear H8.
destruct H0.
rewrite H2 in H0.
injection H0. intros. subst. clear H3.
assert (matr = x).
apply matrix_some_eq.
assumption.
rewrite H3 in H5.
destruct H1.
destruct H1.
assert (Some bb = Some m10).
destruct H6.
destruct H7.
rewrite <- H7.
rewrite <- H5.
reflexivity.
injection H7; intros.
rewrite H8; reflexivity.

destruct X.
unfold equal_id in Heqb.
elim (beq_nat_false n n); auto.

split.
destruct (equal_id X mid0) eqn:?.
inversion H.
apply H0.

split.
apply H0.

unfold invariants; split.

rewrite T1.
apply H0.

split.
rewrite T2.
apply H0.

split.
rewrite T3.
apply H0.

split.
rewrite T4.
apply H0.

split.
rewrite T5.
apply H0.

split.
rewrite T6.
apply H0.

unfold invariants in H0.
apply H0.
Qed.

Theorem hoare_byte_matrix_asgn_11 : forall (mid X: Id) m00 m01 m10 m11, 
                                    equal_id X mid = false -> 
                                    equal_id X mini_sbox_id = false -> 
                                    equal_id X mini_sbox_inv_id = false ->
                                    equal_id X mult_table_id = false ->
                                    equal_id X kid0 = false ->  
                                    equal_id X kid1 = false -> 
                                    equal_id X kid2 = false ->
  {{ fun st => exists (matr: Matrix Byte 2 2),
               st mid = Some (byte_matrix_val matr) /\
               matrix_defined matr m00 m01 m10 m11 /\
               invariants st }}
      byte X ::= (byte_exp_matrix mid 1 1)
  {{ fun st => exists (matr: Matrix Byte 2 2),
               st X = Some (byte_val m11) /\
               st mid = Some (byte_matrix_val matr) /\
               matrix_defined matr m00 m01 m10 m11 /\
               invariants st}}.
Proof.
intros until 0. intros H T1 T2 T3 T4 T5 T6.
eapply hoare_consequence_pre.
apply hoare_asgn.
intros st H1 bb H2.
elim H1; intros x H0; clear H1.
exists x.
split; unfold update.
destruct (equal_id X X) eqn:?. clear Heqb.
inversion H2; subst. clear H2.
inversion H6; subst. clear H6.
inversion H7; subst. clear H7.
inversion H8; subst. clear H8.
destruct H0.
rewrite H2 in H0.
injection H0. intros. subst. clear H3.
assert (matr = x).
apply matrix_some_eq.
assumption.
rewrite H3 in H5.
destruct H1.
destruct H1.
assert (Some bb = Some m11).
destruct H6.
destruct H7.
rewrite <- H8.
rewrite <- H5.
reflexivity.
injection H7; intros.
rewrite H8; reflexivity.

destruct X.
unfold equal_id in Heqb.
elim (beq_nat_false n n); auto.

split.
destruct (equal_id X mid0) eqn:?.
inversion H.
apply H0.

split.
apply H0.

unfold invariants; split.

rewrite T1.
apply H0.

split.
rewrite T2.
apply H0.

split.
rewrite T3.
apply H0.

split.
rewrite T4.
apply H0.

split.
rewrite T5.
apply H0.

split.
rewrite T6.
apply H0.

unfold invariants in H0.
apply H0.
Qed.


Theorem byte_int : forall (j:Integer)(bval:Byte), Some (int_val j) = Some (byte_val bval)
                                                   -> j=bval.
Proof.
intros.
remember (int_val j).
remember (byte_val bval).
injection H.
intros.
subst.
discriminate.
Qed.

Theorem hoare_byte_matrix_asgn_0_id : forall (sboxId mid X id: Id)(sbox:Matrix Byte 1 16) bval sbox_0_id m00 m01 m10 m11, 
                                      equal_id X mid = false ->
                                      equal_id X id = false ->
                                      equal_id X mini_sbox_id = false -> 
                                      equal_id X mini_sbox_inv_id = false ->
                                      equal_id X mult_table_id = false ->
                                      equal_id X kid0 = false ->  
                                      equal_id X kid1 = false -> 
                                      equal_id X kid2 = false ->
                                      get Byte 1 16 0 bval sbox = Some sbox_0_id ->
  {{ fun st => exists (matr: Matrix Byte 2 2),
               st sboxId = Some (byte_matrix_val sbox) /\
               st id = Some (byte_val bval) /\
               st mid = Some (byte_matrix_val matr) /\
               matrix_defined matr m00 m01 m10 m11 /\
               invariants st }}
      byte X ::= (byte_exp_matrix sboxId 0 id)
  {{ fun st => exists (matr: Matrix Byte 2 2),
               st id = Some (byte_val bval) /\
               st X = Some (byte_val sbox_0_id) /\
               st mid = Some (byte_matrix_val matr) /\
               matrix_defined matr m00 m01 m10 m11 /\
               invariants st}}.
Proof.
intros until 0. intros H T1 T2 T3 T4 T5 T6 T7 H0.
eapply hoare_consequence_pre.
apply hoare_asgn.
intros st H' b Hbeval.
elim H'; intros; clear H'.
exists x.
unfold update.

split.
rewrite T1.
apply H1.

split.
destruct (equal_id X X) eqn:?.
inversion Hbeval; subst; clear Hbeval.
inversion H6; subst; clear H6.
inversion H7; subst; clear H7.
inversion H8; subst; clear H8.
destruct H1.
destruct H2.
rewrite H4 in H2.
assert (j = bval).
apply byte_int ; assumption.
subst.
rewrite H3 in H1.
injection H1; intros; subst. clear H7.
assert (matr = sbox).
apply matrix_some_eq.
assumption. subst.
assert (Some b = Some sbox_0_id).
rewrite <- H5. rewrite <- H0.
reflexivity.
injection H7; intros; subst.
reflexivity.

destruct X.
unfold equal_id in *.
elim (beq_nat_false n n); auto.

split.
rewrite H.
apply H1.

split.
apply H1.

unfold invariants.

split.
rewrite T2.
apply H1.

split.
rewrite T3.
apply H1.

split.
rewrite T4.
apply H1.

split.
rewrite T5.
apply H1.

split.
rewrite T6.
apply H1.

split.
rewrite T7.
apply H1.

unfold invariants in H1.
apply H1.
Qed.


Lemma hoare_matrix_matr_10_11 : forall (mid bid:Id)(bval:Byte) m00 m01 m10 m11,
                                   equal_id mid bid = false -> 
                                   equal_id mid mini_sbox_id = false -> 
                                   equal_id mid mini_sbox_inv_id = false ->
                                   equal_id mid mult_table_id = false ->
                                   equal_id mid kid0 = false ->  
                                   equal_id mid kid1 = false -> 
                                   equal_id mid kid2 = false ->
    {{ fun st => exists (matr: Matrix Byte 2 2),
                 st bid = Some (byte_val bval) /\
                 st mid = Some (byte_matrix_val matr) /\
                 matrix_defined matr m00 m01 m10 m11 /\
                 invariants st }}
      instr_matrix_set mid 1 0 (byte_exp_matrix mid 1 1)
    {{ fun st => exists (matr': Matrix Byte 2 2),
                 st bid = Some (byte_val bval) /\
                 st mid = Some (byte_matrix_val matr') /\
                 matrix_defined matr' m00 m01 m11 m11 /\
                 invariants st }}.
Proof.
intros until 0. intros T0 T1 T2 T3 T4 T5 T6.
eapply hoare_consequence_pre.
apply hoare_matrix_set.
intros st H' m n m0 m1 i0 j0 b H2 H3 H4 H0 H1.
elim H'; intros; clear H'.
elim (set_matrix 1 0 2 2 x b); [ intros | omega | omega ].
exists x0.
destruct H. destruct H6.
inversion_clear H0.
inversion H2; subst. clear H2.
inversion H3; subst. clear H3.
rewrite H8 in H6.
injection H6; intros; subst. clear H0.
inversion H4; subst. clear H4.
inversion H11; subst. clear H11.
inversion H12; subst. clear H12.
inversion_clear H10.
rewrite H0 in H8. clear H0.
injection H8; intros; subst. clear H0.
assert (matr = m0 /\ m0 = x).
split; apply matrix_some_eq; assumption.
destruct H0.
subst.
unfold update.

split.
rewrite T0.
apply H.

split.
destruct (equal_id mid0 mid0) eqn:?. clear Heqb0.
assert (Some m1 = Some x0).
rewrite <- H1. rewrite <- H5.
reflexivity.
injection H0; intros; subst; auto.
destruct mid0.
unfold equal_id in Heqb0.
elim (beq_nat_false n n); auto.

split.
destruct H7.
destruct H0.
destruct H3.
destruct H4.
assert (Some b = Some m11).
rewrite <- H7. rewrite <- H9.
reflexivity.
injection H10; intros; subst. clear H10.
apply matrix_get_set_10 with (matr:=x)(m10:=m10).
unfold matrix_defined; repeat split; assumption.
apply H5.

unfold invariants.
split.
rewrite T1.
apply H7.

split.
rewrite T2.
apply H7.

split.
rewrite T3.
apply H7.

split.
rewrite T4.
apply H7.

split.
rewrite T5.
apply H7.

split.
rewrite T6.
apply H7.

unfold invariants in H7.
apply H7.
Qed.

Theorem hoare_matrix_id_00 : forall (bid mid:Id)(bb: Byte) m00 m01 m10 m11, 
                             equal_id mid bid = false ->
                             equal_id mid mini_sbox_id = false -> 
                             equal_id mid mini_sbox_inv_id = false ->
                             equal_id mid mult_table_id = false ->
                             equal_id mid kid0 = false ->  
                             equal_id mid kid1 = false -> 
                             equal_id mid kid2 = false ->
    {{ fun st => exists (matr: Matrix Byte 2 2),
                 st bid = Some (byte_val bb) /\
                 st mid = Some (byte_matrix_val matr) /\
                 matrix_defined matr m00 m01 m10 m11 /\
                 invariants st }}
      instr_matrix_set mid 0 0 bid
    {{ fun st => exists (matr': Matrix Byte 2 2),
                 st bid = Some (byte_val bb) /\
                 st mid = Some (byte_matrix_val matr') /\
                 matrix_defined matr' bb m01 m10 m11 /\
                 invariants st }}.
Proof.
intros until 0. intros H T1 T2 T3 T4 T5 T6.
eapply hoare_consequence_pre.
apply hoare_matrix_set.
intros st H' m n m0 m1 i j b H1 H2 H3 H4 H5.
elim H'; intros; clear H'.
elim (set_matrix 0 0 2 2 x b); intros.
exists x0.
unfold update.
split.

rewrite H.
apply H0.

split.
destruct (equal_id mid0 mid0) eqn:?. clear Heqb0.
destruct H0.
destruct H7.
inversion_clear H4.
inversion H1; subst.
inversion H2; subst.
inversion H3; subst.
rewrite H9 in H7.
clear H1 H2 H3 H9.
injection H7; intros; subst. clear H1. 
assert (Some m1 = Some x0).
replace m0 with x in H5.
elim H6.
rewrite  <- H5. auto.
apply matrix_some_eq.
symmetry. assumption.
injection H1; intros; subst. auto.

destruct mid0.
unfold equal_id in *.
elim (beq_nat_false n0 n0); auto.

split.
inversion_clear H3.
destruct H0.
rewrite H7 in H0.
injection H0; intros; subst. clear H7.
apply matrix_get_set_00 with (matr:=x)(m00:=m00).
apply H3.
apply H6; omega.

unfold invariants.
split.
rewrite T1.
apply H0.

split.
rewrite T2.
apply H0.

split.
rewrite T3.
apply H0.

split.
rewrite T4.
apply H0.

split.
rewrite T5.
apply H0.

split.
rewrite T6.
apply H0.
apply H0.

omega. omega.
Qed.


Theorem hoare_matrix_id_01 : forall (bid mid:Id)(bb: Byte) m00 m01 m10 m11, 
                             equal_id mid bid = false ->
                             equal_id mid mini_sbox_id = false -> 
                             equal_id mid mini_sbox_inv_id = false ->
                             equal_id mid mult_table_id = false ->
                             equal_id mid kid0 = false ->  
                             equal_id mid kid1 = false -> 
                             equal_id mid kid2 = false ->
    {{ fun st => exists (matr: Matrix Byte 2 2),
                 st bid = Some (byte_val bb) /\
                 st mid = Some (byte_matrix_val matr) /\
                 matrix_defined matr m00 m01 m10 m11 /\
                 invariants st }}
      instr_matrix_set mid 0 1 bid
    {{ fun st => exists (matr': Matrix Byte 2 2),
                 st bid = Some (byte_val bb) /\
                 st mid = Some (byte_matrix_val matr') /\
                 matrix_defined matr' m00 bb m10 m11 /\
                 invariants st }}.
Proof.
intros until 0. intros H T1 T2 T3 T4 T5 T6.
eapply hoare_consequence_pre.
apply hoare_matrix_set.
intros st H' m n m0 m1 i j b H1 H2 H3 H4 H5.
elim H'; intros; clear H'.
elim (set_matrix 0 1 2 2 x b); intros.
exists x0.
unfold update.
split.

rewrite H.
apply H0.

split.
destruct (equal_id mid0 mid0) eqn:?. clear Heqb0.
destruct H0.
destruct H7.
inversion_clear H4.
inversion H1; subst.
inversion H2; subst.
inversion H3; subst.
rewrite H9 in H7.
clear H1 H2 H3 H9.
injection H7; intros; subst. clear H1. 
assert (Some m1 = Some x0).
replace m0 with x in H5.
elim H6.
rewrite  <- H5. auto.
apply matrix_some_eq.
symmetry. assumption.
injection H1; intros; subst. auto.

destruct mid0.
unfold equal_id in *.
elim (beq_nat_false n0 n0); auto.

split.
inversion_clear H3.
destruct H0.
rewrite H7 in H0.
injection H0; intros; subst. clear H7.
apply matrix_get_set_01 with (matr:=x)(m01:=m01).
apply H3.
apply H6; omega.

unfold invariants.
split.
rewrite T1.
apply H0.

split.
rewrite T2.
apply H0.

split.
rewrite T3.
apply H0.

split.
rewrite T4.
apply H0.

split.
rewrite T5.
apply H0.

split.
rewrite T6.
apply H0.
apply H0.

omega. omega.
Qed.


Theorem hoare_matrix_id_10 : forall (bid mid:Id)(bb: Byte) m00 m01 m10 m11, 
                             equal_id mid bid = false ->
                             equal_id mid mini_sbox_id = false -> 
                             equal_id mid mini_sbox_inv_id = false ->
                             equal_id mid mult_table_id = false ->
                             equal_id mid kid0 = false ->  
                             equal_id mid kid1 = false -> 
                             equal_id mid kid2 = false ->
    {{ fun st => exists (matr: Matrix Byte 2 2),
                 st bid = Some (byte_val bb) /\
                 st mid = Some (byte_matrix_val matr) /\
                 matrix_defined matr m00 m01 m10 m11 /\
                 invariants st }}
      instr_matrix_set mid 1 0 bid
    {{ fun st => exists (matr': Matrix Byte 2 2),
                 st bid = Some (byte_val bb) /\
                 st mid = Some (byte_matrix_val matr') /\
                 matrix_defined matr' m00 m01 bb m11 /\
                 invariants st }}.
Proof.
intros until 0. intros H T1 T2 T3 T4 T5 T6.
eapply hoare_consequence_pre.
apply hoare_matrix_set.
intros st H' m n m0 m1 i j b H1 H2 H3 H4 H5.
elim H'; intros; clear H'.
elim (set_matrix 1 0 2 2 x b); intros.
exists x0.
unfold update.
split.

rewrite H.
apply H0.

split.
destruct (equal_id mid0 mid0) eqn:?. clear Heqb0.
destruct H0.
destruct H7.
inversion_clear H4.
inversion H1; subst.
inversion H2; subst.
inversion H3; subst.
rewrite H9 in H7.
clear H1 H2 H3 H9.
injection H7; intros; subst. clear H1. 
assert (Some m1 = Some x0).
replace m0 with x in H5.
elim H6.
rewrite  <- H5. auto.
apply matrix_some_eq.
symmetry. assumption.
injection H1; intros; subst. auto.

destruct mid0.
unfold equal_id in *.
elim (beq_nat_false n0 n0); auto.

split.
inversion_clear H3.
destruct H0.
rewrite H7 in H0.
injection H0; intros; subst. clear H7.
apply matrix_get_set_10 with (matr:=x)(m10:=m10).
apply H3.
apply H6; omega.

unfold invariants.
split.
rewrite T1.
apply H0.

split.
rewrite T2.
apply H0.

split.
rewrite T3.
apply H0.

split.
rewrite T4.
apply H0.

split.
rewrite T5.
apply H0.

split.
rewrite T6.
apply H0.
apply H0.

omega. omega.
Qed.

Theorem hoare_matrix_id_11 : forall (bid mid:Id)(bb: Byte) m00 m01 m10 m11, 
                             equal_id mid bid = false ->
                             equal_id mid mini_sbox_id = false -> 
                             equal_id mid mini_sbox_inv_id = false ->
                             equal_id mid mult_table_id = false ->
                             equal_id mid kid0 = false ->  
                             equal_id mid kid1 = false -> 
                             equal_id mid kid2 = false ->
    {{ fun st => exists (matr: Matrix Byte 2 2),
                 st bid = Some (byte_val bb) /\
                 st mid = Some (byte_matrix_val matr) /\
                 matrix_defined matr m00 m01 m10 m11 /\
                 invariants st }}
      instr_matrix_set mid 1 1 bid
    {{ fun st => exists (matr': Matrix Byte 2 2),
                 st bid = Some (byte_val bb) /\
                 st mid = Some (byte_matrix_val matr') /\
                 matrix_defined matr' m00 m01 m10 bb /\
                 invariants st }}.
Proof.
intros until 0. intros H T1 T2 T3 T4 T5 T6.
eapply hoare_consequence_pre.
apply hoare_matrix_set.
intros st H' m n m0 m1 i j b H1 H2 H3 H4 H5.
elim H'; intros; clear H'.
elim (set_matrix 1 1 2 2 x b); intros.
exists x0.
unfold update.
split.

rewrite H.
apply H0.

split.
destruct (equal_id mid0 mid0) eqn:?. clear Heqb0.
destruct H0.
destruct H7.
inversion_clear H4.
inversion H1; subst.
inversion H2; subst.
inversion H3; subst.
rewrite H9 in H7.
clear H1 H2 H3 H9.
injection H7; intros; subst. clear H1. 
assert (Some m1 = Some x0).
replace m0 with x in H5.
elim H6.
rewrite  <- H5. auto.
apply matrix_some_eq.
symmetry. assumption.
injection H1; intros; subst. auto.

destruct mid0.
unfold equal_id in *.
elim (beq_nat_false n0 n0); auto.

split.
inversion_clear H3.
destruct H0.
rewrite H7 in H0.
injection H0; intros; subst. clear H7.
apply matrix_get_set_11 with (matr:=x)(m11:=m11).
apply H3.
apply H6; omega.

unfold invariants.
split.
rewrite T1.
apply H0.

split.
rewrite T2.
apply H0.

split.
rewrite T3.
apply H0.

split.
rewrite T4.
apply H0.

split.
rewrite T5.
apply H0.

split.
rewrite T6.
apply H0.
apply H0.

omega. omega.
Qed.


Lemma hoare_shift_row : forall mid m00 m01 m10 m11,
                        equal_id MiniAes.aux mid = false ->
                        equal_id mid MiniAes.aux = false -> 
                        equal_id mid mini_sbox_id = false -> 
                        equal_id mid mini_sbox_inv_id = false ->
                        equal_id mid mult_table_id = false ->
                        equal_id mid kid0 = false ->  
                        equal_id mid kid1 = false -> 
                        equal_id mid kid2 = false ->
     {{ fun st => exists (matr: Matrix Byte 2 2),
                  st mid = Some (byte_matrix_val matr) /\
                  matrix_defined matr m00 m01 m10 m11 /\
                  invariants st }}
     MiniAes.shift_row mid
     {{ fun st => exists (newMatr: Matrix Byte 2 2),
                  st mid = Some (byte_matrix_val newMatr) /\
                  matrix_defined newMatr m00 m01 m11 m10 /\
                  invariants st }}.
Proof.
intros.
unfold MiniAes.shift_row.

eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_byte_matrix_asgn_10; try equal_id_false.
assumption.

clear H.
intros st H.
elim H; intros; clear H.
exists x.
apply H7.

eapply hoare_seq.
apply hoare_matrix_matr_10_11; try equal_id_false; assumption.

eapply hoare_consequence_post; try equal_id_false.
apply hoare_matrix_id_11; try equal_id_false; assumption.

intros st H7.
elim H7.
intros.
exists x.
destruct H8.
apply H9.
Qed.

Lemma hoare_nibble_sub : forall m00 m01 m10 m11 s00 s01 s10 s11,
           get Byte 1 16 0 m00 mini_sbox = Some s00 ->
           get Byte 1 16 0 m01 mini_sbox = Some s01 ->
           get Byte 1 16 0 m10 mini_sbox = Some s10 ->
           get Byte 1 16 0 m11 mini_sbox = Some s11 ->
           
     {{ fun st => exists (matr: Matrix Byte 2 2),
                  st mid = Some (byte_matrix_val matr) /\
                  matrix_defined matr m00 m01 m10 m11 /\
                  invariants st}}
     MiniAes.nibble_sub mid mini_sbox_id
     {{ fun st => exists (newMatr: Matrix Byte 2 2),
                  st mid = Some (byte_matrix_val newMatr) /\
                  matrix_defined newMatr s00 s01 s10 s11 /\
                  invariants st }}.
Proof.
intros.
unfold MiniAes.nibble_sub.

eapply hoare_seq.
apply hoare_byte_matrix_asgn_00 ; auto.
eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_byte_matrix_asgn_0_id with (sboxId:=mini_sbox_id)(sbox:=mini_sbox); auto.
Focus 2.
apply H.
Focus 2.
intros st H'.
elim H'; intros; clear H'.
exists x.
split.
apply H3.
apply H3.
auto.

eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_matrix_id_00; auto.

intros st H'.
elim H'; intros; clear H'.
exists x.
apply H3.

eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_byte_matrix_asgn_01;try equal_id_false.
auto.
intros st H'.
elim H'; intros; clear H'.
exists x.
apply H3.

eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_byte_matrix_asgn_0_id with (sboxId:=mini_sbox_id)(sbox:=mini_sbox); auto.
Focus 2.
apply H0.
Focus 2.
intros st H'.
elim H'; intros; clear H'.
exists x.
split.
apply H3.
apply H3.
auto.
eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_matrix_id_01; try equal_id_false.
auto.
intros st H'.
elim H'; intros; clear H'.
exists x.
apply H3.

eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_byte_matrix_asgn_10; try equal_id_false.
auto.
intros st H'.
elim H'; intros; clear H'.
exists x.
apply H3.

eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_byte_matrix_asgn_0_id with (sboxId:=mini_sbox_id)(sbox:=mini_sbox);auto.
Focus 2.
apply H1.
Focus 2.
intros st H'.
elim H'; intros; clear H'.
exists x.
split; apply H3.
auto.

eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_matrix_id_10; try equal_id_false.
auto.
intros st H'.
elim H'; intros; clear H'.
exists x.
split; apply H3.

eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_byte_matrix_asgn_11; try equal_id_false.
auto.
intros st H'.
elim H'; intros; clear H'.
exists x.
split; apply H3.

eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_byte_matrix_asgn_0_id with (sboxId:=mini_sbox_id)(sbox:=mini_sbox);auto.
Focus 2.
apply H2.
Focus 2.
intros st H'.
elim H'; intros; clear H'.
exists x.
split; apply H3.
auto.
eapply hoare_consequence_pre.
eapply hoare_consequence_post.
apply hoare_matrix_id_11; try equal_id_false.
auto.
intros st H'.
elim H'; intros; clear H'.
exists x.
split; apply H3.
intros st H'.
elim H'; intros; clear H'.
exists x.
split; apply H3.
Qed.

Lemma hoare_nibble_sub_inv : forall m00 m01 m10 m11 s00 s01 s10 s11,
           get Byte 1 16 0 m00 mini_sbox_inv = Some s00 ->
           get Byte 1 16 0 m01 mini_sbox_inv = Some s01 ->
           get Byte 1 16 0 m10 mini_sbox_inv = Some s10 ->
           get Byte 1 16 0 m11 mini_sbox_inv = Some s11 ->
     {{ fun st => exists (matr: Matrix Byte 2 2),
                  st mid = Some (byte_matrix_val matr) /\
                  matrix_defined matr m00 m01 m10 m11 /\
                  invariants st}}
     MiniAes.nibble_sub mid mini_sbox_inv_id
     {{ fun st => exists (newMatr: Matrix Byte 2 2),
                  st mid = Some (byte_matrix_val newMatr) /\
                  matrix_defined newMatr s00 s01 s10 s11 /\
                  invariants st }}.
Proof.
intros.
unfold MiniAes.nibble_sub.

eapply hoare_seq.
apply hoare_byte_matrix_asgn_00; auto.
eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_byte_matrix_asgn_0_id with (sboxId:=mini_sbox_inv_id)(sbox:=mini_sbox_inv); auto.
Focus 2.
apply H.
Focus 2.
intros st H'.
elim H'; intros; clear H'.
exists x.
split.
unfold invariants in H3.
apply H3.
apply H3.
auto.

eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_matrix_id_00; auto.
intros st H'.
elim H'; intros; clear H'.
exists x.
apply H3.

eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_byte_matrix_asgn_01; try equal_id_false.
auto.
intros st H'.
elim H'; intros; clear H'.
exists x.
apply H3.
eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_byte_matrix_asgn_0_id with (sboxId:=mini_sbox_inv_id)(sbox:=mini_sbox_inv); auto.
Focus 2.
apply H0.
Focus 2.
intros st H'.
elim H'; intros; clear H'.
exists x.
split.
apply H3.
apply H3.
auto.

eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_matrix_id_01; try equal_id_false.
auto.
intros st H'.
elim H'; intros; clear H'.
exists x.
apply H3.

eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_byte_matrix_asgn_10; try equal_id_false.
auto.
intros st H'.
elim H'; intros; clear H'.
exists x.
apply H3.

eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_byte_matrix_asgn_0_id with (sboxId:=mini_sbox_inv_id)(sbox:=mini_sbox_inv);auto.
Focus 2.
apply H1.
Focus 2.
intros st H'.
elim H'; intros; clear H'.
exists x.
split; apply H3.
auto.

eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_matrix_id_10; try equal_id_false.
auto.
intros st H'.
elim H'; intros; clear H'.
exists x.
split; apply H3.

eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_byte_matrix_asgn_11; try equal_id_false.
auto.
intros st H'.
elim H'; intros; clear H'.
exists x.
split; apply H3.

eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_byte_matrix_asgn_0_id with (sboxId:=mini_sbox_inv_id)(sbox:=mini_sbox_inv); auto.
Focus 2.
apply H2.
Focus 2.
intros st H'.
elim H'; intros; clear H'.
exists x.
split; apply H3.
auto.
eapply hoare_consequence_pre.
eapply hoare_consequence_post.
apply hoare_matrix_id_11; try equal_id_false.
auto.
intros st H'.
elim H'; intros; clear H'.
exists x.
split; apply H3.
intros st H'.
elim H'; intros; clear H'.
exists x.
split; apply H3.
Qed.

Theorem hoare_matrix_multable_id_00 : forall (bid1 bid2 mid:Id)(b1 b2 bval: Byte) m00 m01 m10 m11,
                 equal_id mid bid1 = false ->
                 equal_id mid bid2 = false ->
                 equal_id mid mini_sbox_id = false ->  
                 equal_id mid mini_sbox_inv_id = false ->
                 equal_id mid mult_table_id = false ->
                 equal_id mid kid0 = false ->  
                 equal_id mid kid1 = false -> 
                 equal_id mid kid2 = false ->
                 get Byte 16 16 b1 b2 mult_table = Some bval ->
    {{ fun st => exists (matr: Matrix Byte 2 2),
                 st bid1 = Some (byte_val b1) /\
                 st bid2 = Some (byte_val b2) /\
                 st mid = Some (byte_matrix_val matr) /\
                 matrix_defined matr m00 m01 m10 m11 /\
                 invariants st }}
      instr_matrix_set mid 0 0 (byte_exp_matrix mult_table_id bid1 bid2)
    {{ fun st => exists (matr': Matrix Byte 2 2),
                 st bid1 = Some (byte_val b1) /\
                 st bid2 = Some (byte_val b2) /\
                 st mid = Some (byte_matrix_val matr') /\
                 matrix_defined matr' bval m01 m10 m11 /\
                 invariants st }}.
Proof.
intros until 0.
intros T0 T1 T2 T3 T4 T5 T6 T7.
intros.
eapply hoare_consequence_pre.
apply hoare_matrix_set.
intros st H' m n m0 m1 i0 j0 b H2 H3 H4 H0 H1.
elim H'; intros; clear H'.
elim (set_matrix 0 0 2 2 x bval); intros.
exists x0.
unfold update; split.
rewrite T0.
apply H5.
split.
rewrite T1.
apply H5.

split.
destruct (equal_id mid0 mid0) eqn:?.
clear Heqb0.
inversion_clear H0.
inversion H2; subst; clear H2.
inversion H3; subst; clear H3.
inversion H4; subst; clear H4.
inversion H10; subst; clear H10.
inversion H11; subst; clear H11.
inversion_clear H9.
destruct H5.
destruct H5.
destruct H9.
destruct H10.
rewrite H7 in H9.
injection H9; intros; subst. clear H12.
assert (m0 = x).
apply matrix_some_eq.
assumption.
rewrite H12 in H1.
unfold invariants in H11.
destruct H11.
destruct H13.
destruct H14.
rewrite H0 in H14.
injection H14; intros; subst. clear H16 H9.
rewrite H2 in H4. clear H2.
rewrite H3 in H5. clear H3.
assert (i = b1).
apply byte_int; assumption.
assert (j = b2).
apply byte_int; assumption.
assert (matr = mult_table).
apply matrix_some_eq.
assumption.
subst.
rewrite H8 in H.
injection H; intros; subst.
assert (Some m1 = Some x0).
rewrite <- H6. rewrite <- H1.
reflexivity.
injection H2; intros; subst.
reflexivity.

destruct mid0.
unfold equal_id in *.
elim (beq_nat_false n0 n0); auto.

split.
apply matrix_get_set_00 with (matr:=x)(m00:=m00).
apply H5.
apply H6 ; omega.

unfold invariants.

split.
rewrite T2.
apply H5.

split.
rewrite T3.
apply H5.

split.
rewrite T4.
apply H5.

split.
rewrite T5.
apply H5.

split.
rewrite T6.
apply H5.

split.
rewrite T7.
apply H5.

unfold invariants in H1.
apply H5.

omega. omega.
Qed.

Theorem hoare_matrix_multable_id_01 : forall (bid1 bid2 mid:Id)(b1 b2 bval: Byte) m00 m01 m10 m11,
                 equal_id mid bid1 = false ->
                 equal_id mid bid2 = false ->
                 equal_id mid mini_sbox_id = false ->  
                 equal_id mid mini_sbox_inv_id = false ->
                 equal_id mid mult_table_id = false ->
                 equal_id mid kid0 = false ->  
                 equal_id mid kid1 = false -> 
                 equal_id mid kid2 = false ->
                 get Byte 16 16 b1 b2 mult_table = Some bval ->
    {{ fun st => exists (matr: Matrix Byte 2 2),
                 st bid1 = Some (byte_val b1) /\
                 st bid2 = Some (byte_val b2) /\
                 st mid = Some (byte_matrix_val matr) /\
                 matrix_defined matr m00 m01 m10 m11 /\
                 invariants st }}
      instr_matrix_set mid 0 1 (byte_exp_matrix mult_table_id bid1 bid2)
    {{ fun st => exists (matr': Matrix Byte 2 2),
                 st bid1 = Some (byte_val b1) /\
                 st bid2 = Some (byte_val b2) /\
                 st mid = Some (byte_matrix_val matr') /\
                 matrix_defined matr' m00 bval m10 m11 /\
                 invariants st }}.
Proof.
intros until 0.
intros T0 T1 T2 T3 T4 T5 T6 T7.
intros.
eapply hoare_consequence_pre.
apply hoare_matrix_set.
intros st H' m n m0 m1 i0 j0 b H2 H3 H4 H0 H1.
elim H'; intros; clear H'.
elim (set_matrix 0 1 2 2 x bval); intros.
exists x0.
unfold update; split.
rewrite T0.
apply H5.
split.
rewrite T1.
apply H5.

split.
destruct (equal_id mid0 mid0) eqn:?.
clear Heqb0.
inversion_clear H0.
inversion H2; subst; clear H2.
inversion H3; subst; clear H3.
inversion H4; subst; clear H4.
inversion H10; subst; clear H10.
inversion H11; subst; clear H11.
inversion_clear H9.
destruct H5.
destruct H5.
destruct H9.
destruct H10.
rewrite H7 in H9.
injection H9; intros; subst. clear H12.
assert (m0 = x).
apply matrix_some_eq.
assumption.
rewrite H12 in H1.
unfold invariants in H11.
destruct H11.
destruct H13.
destruct H14.
rewrite H0 in H14.
injection H14; intros; subst. clear H16 H9.
rewrite H2 in H4. clear H2.
rewrite H3 in H5. clear H3.
assert (i = b1).
apply byte_int; assumption.
assert (j = b2).
apply byte_int; assumption.
assert (matr = mult_table).
apply matrix_some_eq.
assumption.
subst.
rewrite H8 in H.
injection H; intros; subst.
assert (Some m1 = Some x0).
rewrite <- H6. rewrite <- H1.
reflexivity.
injection H2; intros; subst.
reflexivity.

destruct mid0.
unfold equal_id in *.
elim (beq_nat_false n0 n0); auto.

split.
apply matrix_get_set_01 with (matr:=x)(m01:=m01).
apply H5.
apply H6 ; omega.

unfold invariants.

split.
rewrite T2.
apply H5.

split.
rewrite T3.
apply H5.

split.
rewrite T4.
apply H5.

split.
rewrite T5.
apply H5.

split.
rewrite T6.
apply H5.

split.
rewrite T7.
apply H5.

unfold invariants in H1.
apply H5.

omega. omega.
Qed.

Theorem hoare_matrix_multable_id_10 : forall (bid1 bid2 mid:Id)(b1 b2 bval: Byte) m00 m01 m10 m11,
                 equal_id mid bid1 = false ->
                 equal_id mid bid2 = false ->
                 equal_id mid mini_sbox_id = false ->  
                 equal_id mid mini_sbox_inv_id = false ->
                 equal_id mid mult_table_id = false ->
                 equal_id mid kid0 = false ->  
                 equal_id mid kid1 = false -> 
                 equal_id mid kid2 = false ->
                 get Byte 16 16 b1 b2 mult_table = Some bval ->
    {{ fun st => exists (matr: Matrix Byte 2 2),
                 st bid1 = Some (byte_val b1) /\
                 st bid2 = Some (byte_val b2) /\
                 st mid = Some (byte_matrix_val matr) /\
                 matrix_defined matr m00 m01 m10 m11 /\
                 invariants st }}
      instr_matrix_set mid 1 0 (byte_exp_matrix mult_table_id bid1 bid2)
    {{ fun st => exists (matr': Matrix Byte 2 2),
                 st bid1 = Some (byte_val b1) /\
                 st bid2 = Some (byte_val b2) /\
                 st mid = Some (byte_matrix_val matr') /\
                 matrix_defined matr' m00 m01 bval m11 /\
                 invariants st }}.
Proof.
intros until 0.
intros T0 T1 T2 T3 T4 T5 T6 T7.
intros.
eapply hoare_consequence_pre.
apply hoare_matrix_set.
intros st H' m n m0 m1 i0 j0 b H2 H3 H4 H0 H1.
elim H'; intros; clear H'.
elim (set_matrix 1 0 2 2 x bval); intros.
exists x0.
unfold update; split.
rewrite T0.
apply H5.
split.
rewrite T1.
apply H5.

split.
destruct (equal_id mid0 mid0) eqn:?.
clear Heqb0.
inversion_clear H0.
inversion H2; subst; clear H2.
inversion H3; subst; clear H3.
inversion H4; subst; clear H4.
inversion H10; subst; clear H10.
inversion H11; subst; clear H11.
inversion_clear H9.
destruct H5.
destruct H5.
destruct H9.
destruct H10.
rewrite H7 in H9.
injection H9; intros; subst. clear H12.
assert (m0 = x).
apply matrix_some_eq.
assumption.
rewrite H12 in H1.
unfold invariants in H11.
destruct H11.
destruct H13.
destruct H14.
rewrite H0 in H14.
injection H14; intros; subst. clear H16 H9.
rewrite H2 in H4. clear H2.
rewrite H3 in H5. clear H3.
assert (i = b1).
apply byte_int; assumption.
assert (j = b2).
apply byte_int; assumption.
assert (matr = mult_table).
apply matrix_some_eq.
assumption.
subst.
rewrite H8 in H.
injection H; intros; subst.
assert (Some m1 = Some x0).
rewrite <- H6. rewrite <- H1.
reflexivity.
injection H2; intros; subst.
reflexivity.

destruct mid0.
unfold equal_id in *.
elim (beq_nat_false n0 n0); auto.

split.
apply matrix_get_set_10 with (matr:=x)(m10:=m10).
apply H5.
apply H6 ; omega.

unfold invariants.

split.
rewrite T2.
apply H5.

split.
rewrite T3.
apply H5.

split.
rewrite T4.
apply H5.

split.
rewrite T5.
apply H5.

split.
rewrite T6.
apply H5.

split.
rewrite T7.
apply H5.

unfold invariants in H1.
apply H5.

omega. omega.
Qed.


Theorem hoare_matrix_multable_id_11 : forall (bid1 bid2 mid:Id)(b1 b2 bval: Byte) m00 m01 m10 m11,
                 equal_id mid bid1 = false ->
                 equal_id mid bid2 = false ->
                 equal_id mid mini_sbox_id = false ->  
                 equal_id mid mini_sbox_inv_id = false ->
                 equal_id mid mult_table_id = false ->
                 equal_id mid kid0 = false ->  
                 equal_id mid kid1 = false -> 
                 equal_id mid kid2 = false ->
                 get Byte 16 16 b1 b2 mult_table = Some bval ->
    {{ fun st => exists (matr: Matrix Byte 2 2),
                 st bid1 = Some (byte_val b1) /\
                 st bid2 = Some (byte_val b2) /\
                 st mid = Some (byte_matrix_val matr) /\
                 matrix_defined matr m00 m01 m10 m11 /\
                 invariants st }}
      instr_matrix_set mid 1 1 (byte_exp_matrix mult_table_id bid1 bid2)
    {{ fun st => exists (matr': Matrix Byte 2 2),
                 st bid1 = Some (byte_val b1) /\
                 st bid2 = Some (byte_val b2) /\
                 st mid = Some (byte_matrix_val matr') /\
                 matrix_defined matr' m00 m01 m10 bval /\
                 invariants st }}.
Proof.
intros until 0.
intros T0 T1 T2 T3 T4 T5 T6 T7.
intros.
eapply hoare_consequence_pre.
apply hoare_matrix_set.
intros st H' m n m0 m1 i0 j0 b H2 H3 H4 H0 H1.
elim H'; intros; clear H'.
elim (set_matrix 1 1 2 2 x bval); intros.
exists x0.
unfold update; split.
rewrite T0.
apply H5.
split.
rewrite T1.
apply H5.

split.
destruct (equal_id mid0 mid0) eqn:?.
clear Heqb0.
inversion_clear H0.
inversion H2; subst; clear H2.
inversion H3; subst; clear H3.
inversion H4; subst; clear H4.
inversion H10; subst; clear H10.
inversion H11; subst; clear H11.
inversion_clear H9.
destruct H5.
destruct H5.
destruct H9.
destruct H10.
rewrite H7 in H9.
injection H9; intros; subst. clear H12.
assert (m0 = x).
apply matrix_some_eq.
assumption.
rewrite H12 in H1.
unfold invariants in H11.
destruct H11.
destruct H13.
destruct H14.
rewrite H0 in H14.
injection H14; intros; subst. clear H16 H9.
rewrite H2 in H4. clear H2.
rewrite H3 in H5. clear H3.
assert (i = b1).
apply byte_int; assumption.
assert (j = b2).
apply byte_int; assumption.
assert (matr = mult_table).
apply matrix_some_eq.
assumption.
subst.
rewrite H8 in H.
injection H; intros; subst.
assert (Some m1 = Some x0).
rewrite <- H6. rewrite <- H1.
reflexivity.
injection H2; intros; subst.
reflexivity.

destruct mid0.
unfold equal_id in *.
elim (beq_nat_false n0 n0); auto.

split.
apply matrix_get_set_11 with (matr:=x)(m11:=m11).
apply H5.
apply H6 ; omega.

unfold invariants.

split.
rewrite T2.
apply H5.

split.
rewrite T3.
apply H5.

split.
rewrite T4.
apply H5.

split.
rewrite T5.
apply H5.

split.
rewrite T6.
apply H5.

split.
rewrite T7.
apply H5.

unfold invariants in H1.
apply H5.

omega. omega.
Qed.

Theorem hoare_byte_matrix_asgn_10_bid : forall (bid mid X: Id) bb m00 m01 m10 m11, 
                                        equal_id X mid = false ->
                                        equal_id X bid = false ->
                                        equal_id X mini_sbox_id = false ->  
                                        equal_id X mini_sbox_inv_id = false ->
                                        equal_id X mult_table_id = false ->
                                        equal_id X kid0 = false ->  
                                        equal_id X kid1 = false -> 
                                        equal_id X kid2 = false ->
  {{ fun st => exists (matr: Matrix Byte 2 2),
               st bid = Some (byte_val bb) /\
               st mid = Some (byte_matrix_val matr) /\
               matrix_defined matr m00 m01 m10 m11 /\
               invariants st }}
      byte X ::= (byte_exp_matrix mid 1 0)
  {{ fun st => exists (matr: Matrix Byte 2 2),
               st bid = Some (byte_val bb) /\
               st X = Some (byte_val m10) /\
               st mid = Some (byte_matrix_val matr) /\
               matrix_defined matr m00 m01 m10 m11 /\
               invariants st}}.
Proof.
intros until 0.
intros H T1 T2 T3 T4 T5 T6 T7.
eapply hoare_consequence_pre.
apply hoare_asgn.
intros st H1 bval H2.
elim H1; intros; clear H1.
exists x.
split; unfold update.
rewrite T1.
apply H0.

split.
destruct (equal_id X X) eqn:?. clear Heqb.
inversion H2; subst. clear H2.
inversion H6; subst. clear H6.
inversion H7; subst. clear H7.
inversion H8; subst. clear H8.
destruct H0.
destruct H1.
rewrite H2 in H1.
injection H1; intros; subst. clear H4.
assert (matr = x).
apply matrix_some_eq.
assumption.
rewrite H4 in H5.
destruct H3.
destruct H3.
destruct H7.
destruct H8.
assert (Some bval = Some m10).
rewrite <- H5.
rewrite <- H8.
reflexivity.
injection H10; intros.
rewrite H11; reflexivity.

destruct X.
unfold equal_id in *.
elim (beq_nat_false n n); auto.

split.
destruct (equal_id X mid0) eqn:?.
inversion H.
apply H0.

split.
apply H0.

unfold invariants; split.

rewrite T2.
apply H0.

split.
rewrite T3.
apply H0.

split.
rewrite T4.
apply H0.

split.
rewrite T5.
apply H0.

split.
rewrite T6.
apply H0.

split.
rewrite T7.
apply H0.

unfold invariants in H0.
apply H0.
Qed.

Theorem hoare_byte_matrix_asgn_11_bid : forall (bid mid X: Id) bb m00 m01 m10 m11, 
                                        equal_id X mid = false ->
                                        equal_id X bid = false ->
                                        equal_id X mini_sbox_id = false ->  
                                        equal_id X mini_sbox_inv_id = false ->
                                        equal_id X mult_table_id = false ->
                                        equal_id X kid0 = false ->  
                                        equal_id X kid1 = false -> 
                                        equal_id X kid2 = false ->
  {{ fun st => exists (matr: Matrix Byte 2 2),
               st bid = Some (byte_val bb) /\
               st mid = Some (byte_matrix_val matr) /\
               matrix_defined matr m00 m01 m10 m11 /\
               invariants st }}
      byte X ::= (byte_exp_matrix mid 1 1)
  {{ fun st => exists (matr: Matrix Byte 2 2),
               st bid = Some (byte_val bb) /\
               st X = Some (byte_val m11) /\
               st mid = Some (byte_matrix_val matr) /\
               matrix_defined matr m00 m01 m10 m11 /\
               invariants st}}.
Proof.
intros until 0.
intros H T1 T2 T3 T4 T5 T6 T7.
eapply hoare_consequence_pre.
apply hoare_asgn.
intros st H1 bval H2.
elim H1; intros; clear H1.
exists x.
split; unfold update.
rewrite T1.
apply H0.

split.
destruct (equal_id X X) eqn:?. clear Heqb.
inversion H2; subst. clear H2.
inversion H6; subst. clear H6.
inversion H7; subst. clear H7.
inversion H8; subst. clear H8.
destruct H0.
destruct H1.
rewrite H2 in H1.
injection H1; intros; subst. clear H4.
assert (matr = x).
apply matrix_some_eq.
assumption.
rewrite H4 in H5.
destruct H3.
destruct H3.
destruct H7.
destruct H8.
assert (Some bval = Some m11).
rewrite <- H5.
rewrite <- H9.
reflexivity.
injection H10; intros.
rewrite H11; reflexivity.

destruct X.
unfold equal_id in *.
elim (beq_nat_false n n); auto.

split.
destruct (equal_id X mid0) eqn:?.
inversion H.
apply H0.

split.
apply H0.

unfold invariants; split.

rewrite T2.
apply H0.

split.
rewrite T3.
apply H0.

split.
rewrite T4.
apply H0.

split.
rewrite T5.
apply H0.

split.
rewrite T6.
apply H0.

split.
rewrite T7.
apply H0.

unfold invariants in H0.
apply H0.
Qed.

Lemma hoare_mix_columns : forall m00 m01 m10 m11 s00 s01 s10 s11,
           get Byte 16 16 m00 m10 mult_table = Some s00 ->
           get Byte 16 16 m01 m11 mult_table = Some s01 ->
           get Byte 16 16 m10 m00 mult_table = Some s10 ->
           get Byte 16 16 m11 m01 mult_table = Some s11 ->
     {{ fun st => exists (matr: Matrix Byte 2 2),
                  st mid = Some (byte_matrix_val matr) /\
                  matrix_defined matr m00 m01 m10 m11 /\
                  invariants st}}
     MiniAes.mix_columns mid mult_table_id
     {{ fun st => exists (newMatr: Matrix Byte 2 2),
                  st mid = Some (byte_matrix_val newMatr) /\
                  matrix_defined newMatr s00 s01 s10 s11 /\
                  invariants st }}.
Proof.
intros.
unfold MiniAes.mix_columns.
eapply hoare_seq.
apply hoare_byte_matrix_asgn_00; auto.

eapply hoare_seq.
apply hoare_byte_matrix_asgn_10_bid; auto.
eapply hoare_seq.
apply hoare_matrix_multable_id_00; auto.
apply H.

eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_matrix_multable_id_10; try equal_id_false.
apply H1.
intros st H'.
elim H'; intros; clear H'.
exists x.
split.
apply H3.
split.
apply H3.
apply H3.

eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_byte_matrix_asgn_01; try equal_id_false.
intros st H'.
elim H'; intros; clear H'.
exists x.
apply H3.

eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_byte_matrix_asgn_11_bid; try equal_id_false.
Focus 2.
intros st H'.
elim H'; intros; clear H'.
exists x.
apply H3.
auto.

eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_matrix_multable_id_01; try equal_id_false.
apply H0.
intros st H'.
elim H'; intros; clear H'.
exists x.
apply H3.

eapply hoare_consequence_pre.
eapply hoare_consequence_post.
apply hoare_matrix_multable_id_11; try equal_id_false.
apply H2.
intros st H'.
elim H'; intros; clear H'.
exists x.
apply H3.
intros st H'.
elim H'; intros; clear H'.
exists x.
split.
apply H3.
split.
apply H3.
apply H3.
Qed.

Ltac matrix_size :=
  match goal with
    | [|- _ <= _ < _] => omega

    | [|- _ >= _] => omega

    | [|- _ <= _ < _] =>
      first [
        apply nibble_xor |
        apply k0_defined |
        apply k1_defined |
        apply k2_defined |
        assumption
      ]

    | [_: get Byte 1 16 0 ?x mini_sbox = Some ?y |- 0 <= ?y < 16] =>
      apply (mini_sbox_result x); [ assumption | apply nibble_xor | assumption ]

    | [_: get Byte 1 16 0 ?x mini_sbox_inv = Some ?y |- 0 <= ?y < 16] =>
      apply (mini_sbox_inv_result x); [ assumption | apply nibble_xor | assumption ]

    | [_: get Byte 16 16 ?x ?y mult_table = Some ?z |- 0 <= ?z < 16] =>
      apply (mult_table_result x y); [assumption | | | assumption]
  end
.

Theorem hoare_miniaes : forall m00 m01 m10 m11,
          0 <= m00 < 16 ->
          0 <= m01 < 16 ->
          0 <= m10 < 16 ->
          0 <= m11 < 16 ->
          sbox_defined mini_sbox ->
          sbox_inv_defined mini_sbox_inv ->
          mult_table_defined mult_table ->
     {{ fun st => exists (matr: Matrix Byte 2 2),
                  st mid = Some (byte_matrix_val matr) /\
                  matrix_defined matr m00 m01 m10 m11 /\
                  invariants st }}
     MiniAes.encrypt mid mini_sbox_id mult_table_id kid0 kid1 kid2;
     MiniAes.decrypt mid mini_sbox_inv_id mult_table_id kid0 kid1 kid2
     {{ fun st =>  exists (newMatr: Matrix Byte 2 2),
                  st mid = Some (byte_matrix_val newMatr) /\
                  matrix_defined newMatr m00 m01 m10 m11 /\
                  invariants st }}.
Proof.
intros until 0. intros T0 T1 T2 T3 T4 T5 T6.
unfold MiniAes.encrypt.
unfold MiniAes.decrypt.

(* Introduzco variables para usar en 2. *)
elim (get_some 1 16 0 (xor m00 k2_00) mini_sbox); repeat matrix_size.
intros x0 H0.
elim (get_some 1 16 0 (xor m01 k2_01) mini_sbox); repeat matrix_size.
intros x1 H1.
elim (get_some 1 16 0 (xor m10 k2_10) mini_sbox); repeat matrix_size.
intros x2 H2.
elim (get_some 1 16 0 (xor m11 k2_11) mini_sbox); repeat matrix_size.
intros x3 H3.
(* Introduzco variables para usar en 4. *)
elim (get_some 16 16 x0 x3 mult_table); [repeat matrix_size|omega|omega|repeat matrix_size | repeat matrix_size].
intros x4 H4.
elim (get_some 16 16 x1 x2 mult_table); [repeat matrix_size|omega|omega|repeat matrix_size | repeat matrix_size].
intros x5 H5.
elim (get_some 16 16 x3 x0 mult_table); [repeat matrix_size|omega|omega|repeat matrix_size | repeat matrix_size].
intros x6 H6.
elim (get_some 16 16 x2 x1 mult_table); [repeat matrix_size|omega|omega|repeat matrix_size | repeat matrix_size].
intros x7 H7.
(* Introduzco variables para usar en 7. *)
elim (get_some 1 16 0 (xor x4 k1_00) mini_sbox); [repeat matrix_size|omega|omega|repeat matrix_size | repeat matrix_size].
intros x8 H8.
elim (get_some 1 16 0 (xor x5 k1_01) mini_sbox); repeat matrix_size.
intros x9 H9.
elim (get_some 1 16 0 (xor x6 k1_10) mini_sbox); [repeat matrix_size|omega|omega|repeat matrix_size | repeat matrix_size].
intros x10 H10.
elim (get_some 1 16 0 (xor x7 k1_11) mini_sbox); [repeat matrix_size|omega|omega|repeat matrix_size | repeat matrix_size].
intros x11 H11.
(* Introduzco variables para usar en 10. *)
elim (get_some 1 16 0 (xor (xor x8 k0_00) k0_00) mini_sbox_inv); [repeat matrix_size|omega|omega|repeat matrix_size | repeat matrix_size].
intros x12 H12.
elim (get_some 1 16 0 (xor (xor x9 k0_01) k0_01) mini_sbox_inv); [repeat matrix_size|omega|omega|repeat matrix_size | repeat matrix_size].
intros x13 H13.
elim (get_some 1 16 0 (xor (xor x11 k0_10) k0_10) mini_sbox_inv); [repeat matrix_size|omega|omega|repeat matrix_size | repeat matrix_size].
intros x15 H15.
elim (get_some 1 16 0 (xor (xor x10 k0_11) k0_11) mini_sbox_inv); [repeat matrix_size|omega|omega|repeat matrix_size | repeat matrix_size].
intros x14 H14.
(* Introduzco variables para usar en 13 *)
elim (get_some 16 16 (xor x12 k1_00) (xor x14 k1_10) mult_table); [repeat matrix_size|omega|omega|repeat matrix_size | repeat matrix_size].
intros x16 H16.
elim (get_some 16 16 (xor x13 k1_01) (xor x15 k1_11) mult_table); [repeat matrix_size|omega|omega|repeat matrix_size | repeat matrix_size].
intros x17 H17.
elim (get_some 16 16 (xor x14 k1_10) (xor x12 k1_00) mult_table); [repeat matrix_size|omega|omega|repeat matrix_size | repeat matrix_size].
intros x18 H18.
elim (get_some 16 16 (xor x15 k1_11) (xor x13 k1_01) mult_table); [repeat matrix_size|omega|omega|repeat matrix_size | repeat matrix_size].
intros x19 H19.
(* Introduzco variables para usar en 15 *)
elim (get_some 1 16 0 x16 mini_sbox_inv); [repeat matrix_size|omega|omega|repeat matrix_size | repeat matrix_size].
intros x20 H20.
elim (get_some 1 16 0 x17 mini_sbox_inv); [repeat matrix_size|omega|omega|repeat matrix_size | repeat matrix_size].
intros x21 H21.
elim (get_some 1 16 0 x19 mini_sbox_inv); [repeat matrix_size|omega|omega|repeat matrix_size | repeat matrix_size].
intros x22 H22.
elim (get_some 1 16 0 x18 mini_sbox_inv); [repeat matrix_size|omega|omega|repeat matrix_size | repeat matrix_size].
intros x23 H23.

(* 1. key_addition key2 *)
eapply hoare_seq.
eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_key_addition with (key:=key2)(kid:=kid2)(k00:=k2_00)(k01:=k2_01)(k10:=k2_10)(k11:=k2_11).
compute. reflexivity.
intros st H.
elim H; intros; subst. clear H.
exists x.
split.
apply H24.
split. apply H24.
split. apply H24.
split. apply H24.
split. apply H24.
apply H24.

(* 2. nibble_sub *)
eapply hoare_seq.
apply hoare_nibble_sub with (s00:=x0)(s01:=x1)(s10:=x2)(s11:=x3); assumption.

(* 3. shift_row *)
eapply hoare_seq.
apply hoare_shift_row ; auto.

(* 4. mix_columns *)
eapply hoare_seq.
apply hoare_mix_columns with (s00:=x4)(s01:=x5)(s10:=x6)(s11:=x7); assumption.


(* 5. key_addition k1 *)
eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_key_addition with (kid:=kid1)(k00:=k1_00)(k01:=k1_01)(k10:=k1_10)(k11:=k1_11).
compute. reflexivity.
intros st H.
elim H; intros; subst. clear H.
exists x.
split.
apply H24.
split. apply H24.
split. apply H24.
split. apply H24.
split. apply H24.
apply H24.

(* 7. nibble_sub *)
eapply hoare_seq.
apply hoare_nibble_sub with (s00:=x8)(s01:=x9)(s10:=x10)(s11:=x11); assumption.

(* 6. shift_row *)
eapply hoare_seq.
apply hoare_shift_row; auto.

(* 8. key_addition k0 *)
eapply hoare_consequence_pre.
apply hoare_key_addition with (kid:=kid0)(k00:=k0_00)(k01:=k0_01)(k10:=k0_10)(k11:=k0_11).
compute. reflexivity.
intros st H.
elim H; intros; subst. clear H.
exists x.
split.
apply H24.
split. apply H24.
split. apply H24.
split. apply H24.
split. apply H24.
apply H24.

(* 9. key_addition k0 *)
eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_key_addition with (kid:=kid0)(k00:=k0_00)(k01:=k0_01)(k10:=k0_10)(k11:=k0_11).
compute. reflexivity.
intros st H.
elim H; intros; subst. clear H.
exists x.
split.
apply H24.
split. apply H24.
split. apply H24.
split. apply H24.
split. apply H24.
apply H24.

(* 11. shift_row *)
eapply hoare_seq.
apply hoare_shift_row; auto.

(* 10. nibble_sub_inv *)
eapply hoare_seq.
apply hoare_nibble_sub_inv with (s00:=x12)(s01:=x13)(s10:=x14)(s11:=x15); assumption.

(* 12. key_addition *)
eapply hoare_seq.
eapply hoare_consequence_pre.
apply hoare_key_addition with (kid:=kid1)(k00:=k1_00)(k01:=k1_01)(k10:=k1_10)(k11:=k1_11).
compute. reflexivity.
intros st H.
elim H; intros; subst. clear H.
exists x.
split.
apply H24.
split. apply H24.
split. apply H24.
split. apply H24.
split. apply H24.
apply H24.

(* 13. mix_columns *)
eapply hoare_seq.
apply hoare_mix_columns with (s00:=x16)(s01:=x17)(s10:=x18)(s11:=x19); assumption.

(* 14. shift_row *)
eapply hoare_seq.
apply hoare_shift_row; auto.

(* 15. nibble_sub_inv *)
eapply hoare_seq.
apply hoare_nibble_sub_inv with (s00:=x20)(s01:=x21)(s10:=x22)(s11:=x23); assumption.

(* 16. key_addition *)
eapply hoare_consequence_post.
eapply hoare_consequence_pre.
apply hoare_key_addition with (kid:=kid2)(k00:=k2_00)(k01:=k2_01)(k10:=k2_10)(k11:=k2_11).
compute. reflexivity.
intros st H.
elim H; intros; subst. clear H.
exists x.
split.
apply H24.
split. apply H24.
split. apply H24.
split. apply H24.
split. apply H24.
apply H24.

intros st H.
elim H; intros; clear H.
exists x.
split.
apply H24.
split.
Focus 2.
apply H24.

rewrite xor_inverse in *.

rewrite (mini_sbox_inverse (xor x4 k1_00) x8) in H12; [ | assumption | assumption | repeat matrix_size | assumption].
injection H12. intros. subst.
rewrite (mini_sbox_inverse (xor x5 k1_01) x9) in H13; [ | assumption | assumption | repeat matrix_size | assumption].
injection H13. intros. subst.
rewrite (mini_sbox_inverse (xor x6 k1_10) x10) in H14; [ | assumption | assumption | repeat matrix_size | assumption].
injection H14. intros. subst.
rewrite (mini_sbox_inverse (xor x7 k1_11) x11) in H15; [ | assumption | assumption | repeat matrix_size | assumption].
injection H15. intros. subst.
rewrite xor_inverse in *.
rewrite xor_inverse in *.
clear H8 H9 H10 H11 H12 H13 H14 H15.
assert (get Byte 16 16 x4 x6 mult_table = Some x0 /\ get Byte 16 16 x6 x4 mult_table = Some x3).
apply mult_table_inv; [assumption | repeat matrix_size | repeat matrix_size | assumption | assumption ].

destruct H.
rewrite H in H16.
rewrite H8 in H18.
injection H16. intros.
injection H18. intros.
clear H16 H18.
rewrite H9 in H0. clear H9.
rewrite H10 in H3. clear H10.
assert (get Byte 16 16 x5 x7 mult_table = Some x1 /\ get Byte 16 16 x7 x5 mult_table = Some x2).
apply mult_table_inv; [assumption | repeat matrix_size | repeat matrix_size | assumption | assumption ].
destruct H9.
rewrite H9 in H17.
rewrite H10 in H19.
injection H17. intros.
injection H19. intros.
clear H17 H19.
rewrite H11 in H1. clear H11.
rewrite H12 in H2. clear H12.
rewrite (mini_sbox_inverse (xor m00 k2_00) x16) in H20; [ | assumption | assumption | repeat matrix_size | assumption].
injection H20. intros. subst.
rewrite (mini_sbox_inverse (xor m01 k2_01) x17) in H21; [ | assumption | assumption | repeat matrix_size | assumption].
injection H21. intros. subst.
rewrite (mini_sbox_inverse (xor m10 k2_10) x19) in H22; [ | assumption | assumption | repeat matrix_size | assumption].
injection H22. intros. subst.
rewrite (mini_sbox_inverse (xor m11 k2_11) x18) in H23; [ | assumption | assumption | repeat matrix_size | assumption].
injection H23. intros. subst.
rewrite xor_inverse in *.
rewrite xor_inverse in *.
rewrite xor_inverse in *.
rewrite xor_inverse in *.
apply H24.
Qed.
